Nuprl Lemma : sorted-merge
0,22
postcript
pdf
T
:Type.
T
(
bs
,
as
:
T
List. sorted(
as
)
sorted(merge(
as
;
bs
)))
latex
Definitions
t
T
,
P
Q
,
x
:
A
.
B
(
x
)
,
sorted(
L
)
,
merge(
as
;
bs
)
,
S
T
Lemmas
sorted
wf
,
s-insert-sorted
,
merge
wf
origin
T:Type. T 
(bs, as:T List. sorted(as) sorted(merge(as;bs))) T:Type. T (bs, as:T List. sorted(as) sorted(merge(as;bs))) 
T Qx:A. B(x) T